// SAT3.cpp : Defines the entry point for the console application.
//

#include "stdafx.h"
#include <Runtime.Low/Pipeline/Pipeline.h>
#include <fstream>
#include <vector>
#include <set>
#include <algorithm>
#include <iostream>

using std::set;
using std::vector;
using namespace TTGLib::Pipeline;

int varsNum;

struct ConjInfo {
	int q;
	int vars[3];
	ConjInfo(int *a, int l) {
		q = l;
		memcpy(vars, a, sizeof(*vars) * q);
	}
};

template <class T>
inline bool absComp(const T& a, const T& b) {
	return abs(a) < abs(b);
}

struct Group {
private:
	void addUsed(int *a, int l) {
		int *newUsedVars = new int[usedVarsLen + l];
		if (usedVars) {
			usedVarsLen = std::set_union(usedVars, usedVars + usedVarsLen, a, a+l, newUsedVars, absComp<int>) - newUsedVars;
			delete[] usedVars;
			usedVars = newUsedVars;
		} else {
			usedVarsLen = l;
			memcpy(newUsedVars, a, sizeof(*newUsedVars) * l);
			usedVars = newUsedVars;
		}
	}
	void addConj(const ConjInfo &ci) {
		conjsLen++;
		conjs = (ConjInfo *)realloc(conjs, sizeof(ConjInfo) * conjsLen);
		new(conjs+conjsLen-1) ConjInfo(ci);
	}
public:
	bool solved;
	ConjInfo *conjs;
	int conjsLen;
	int *usedVars;
	int usedVarsLen;
	void init() {
		usedVars = NULL;
		usedVarsLen = 0;
		conjs = NULL;
		conjsLen = 0;
		solved = false;
	}
	Group() {init();}
	Group(int *a, int l) {
		init();
		add(a, l);
	}
	void add(int *a, int l) {
		addUsed(a, l);
		addConj(ConjInfo(a, l));
	}
	void merge(const Group &g) {
		addUsed(g.usedVars, g.usedVarsLen);
		for (int i = 0; i < g.conjsLen; i++ )
			addConj(g.conjs[i]);
	}
	void clearUsed() {
		delete[] usedVars;
		usedVars = NULL;
		usedVarsLen = 0;
	}
	void freeMem() {
		clearUsed();
		if (conjs)
			free(conjs);
		conjs = NULL;
		conjsLen = 0;
	}
};

class GroupInst {
	Group *gr;
	int conjsLeft;
public:
	int *vars;
	GroupInst setVal(int varVal) {
		vars[abs(varVal)] = varVal;
		return (*this);
	}
	GroupInst(GroupInst &gi, int varVal):gr(gi.gr), conjsLeft(gi.conjsLeft) {
		vars = new int[varsNum + 1];
		memcpy(vars, gi.vars, sizeof(int) * (varsNum + 1));
		setVal(varVal);
	}
	GroupInst(Group &g):gr(&g),conjsLeft(g.conjsLen) {
		vars = new int[varsNum + 1];
		memset(vars, 0, sizeof(int) * (varsNum + 1));
	}
	bool haveConj() {
		return conjsLeft > 0;
	}
	int getConjsLeft() {
		return conjsLeft;
	}
	ConjInfo popConj() {
		conjsLeft--;
		return gr->conjs[conjsLeft];
	}
	void markAsSolved() {
		gr->solved = true;
	}
	bool isSolved() {
		return gr->solved;
	}
	void freeMem() {
		delete[] vars;
		vars = NULL;
	}
};

class ReaderSplitter: public Node<std::pair<std::istream *, vector<Group> *>, GroupInst> {
	protected:
		void process(std::pair<std::istream *, vector<Group> *> inPair) {
			int N, K;
			std::istream &in = *inPair.first;
			vector<Group> &groups = *inPair.second;
//			groups.clear();
			in >> N >> K;
			varsNum = N;
			for (int kidx = 0; kidx < K; kidx++) {
				int vars[3];
				int q = 3;
				int tmpRes[3];
				in >> vars[0] >> vars[1] >> vars[2];
				if (vars[0] == -vars[1] || vars[1] == -vars[2] || vars[2] == -vars[0])
					continue;
				if (vars[2] == vars[0] || vars[2] == vars[1]) q--;
				if (vars[0] == vars[1]) {
					vars[1] = vars[2];
					q--;
				}
				sort(vars, vars + q, absComp<int>);
				set<size_t> intersectedGroups;
				for (size_t i = 0; i < groups.size(); i++)
					if (std::set_intersection(vars, vars + q, groups[i].usedVars, groups[i].usedVars + groups[i].usedVarsLen, tmpRes, absComp<int>) > tmpRes)
						intersectedGroups.insert(i);
				if (intersectedGroups.size() == 0) {
					groups.push_back(Group(vars, q));
				} else {
					size_t firstIdx = *(intersectedGroups.begin());
					groups[firstIdx].add(vars, q);
					intersectedGroups.erase(intersectedGroups.begin());
					while (intersectedGroups.size()) {
						set<size_t>::iterator it = intersectedGroups.end();
						it--;
						groups[firstIdx].merge(groups[*it]);
						groups[*it].freeMem();
						if (*it != groups.size() - 1) {
							groups[*it] = groups[groups.size() - 1];
						}
						groups.pop_back();
						intersectedGroups.erase(it);
					}
				}
			}
			std::cout<<groups.size()<<" groups total"<<std::endl;
			for (size_t i = 0; i < groups.size(); i++) {
				groups[i].clearUsed();
				sendNext(GroupInst(groups[i]));
			}
		}
};

class SolverDPLL: Node<GroupInst, GroupInst> {
	protected:
		void process(GroupInst gi) {
			processD(gi);
			//int i=10000000;
			//while(i-->0);
		}
		void processD(GroupInst gi, int d = 100000, bool allowFree = true) {
			if (gi.isSolved()) {
				if (allowFree)
					gi.freeMem();
				return;
			}
			if (!gi.haveConj()) {
				gi.markAsSolved();
				if (allowFree)
					sendNext(gi);
				else
					sendNext(GroupInst(gi, 0));
				return;
			}
			ConjInfo ci = gi.popConj();
			bool ciVal = false;
			vector<int> freeVars;
			for (int i = 0; i < ci.q; i++)
				if (gi.vars[abs(ci.vars[i])])
					ciVal = ciVal || gi.vars[abs(ci.vars[i])] == ci.vars[i];
				else
					freeVars.push_back(i);
			int freeVarsCount = freeVars.size();
			if (!ciVal) {
				if (freeVarsCount > 0) {
					int newD = (d - 1) / freeVarsCount;
					for (size_t i = 0; i < freeVarsCount - 1; i++)
						if (newD > 0) {
							processD(gi.setVal(ci.vars[freeVars[i]]), newD, false);
							gi.vars[abs(ci.vars[freeVars[i]])] = 0;
						} else
							sendThis(GroupInst(gi, ci.vars[freeVars[i]]));
					if (newD > 0)
						processD(gi.setVal(ci.vars[freeVars[freeVarsCount - 1]]), newD, allowFree);
					else
						if (allowFree)
							sendThis(gi.setVal(ci.vars[freeVars[freeVarsCount - 1]]));
						else
							sendThis(GroupInst(gi, ci.vars[freeVars[freeVarsCount -1]]));
				} else
					if (allowFree)
						gi.freeMem();
			} else
				processD(gi, d - 1, allowFree);
		}
		long getDifficulty(GroupInst gi) {
			return (1<<30) - gi.getConjsLeft();
		}
};

class Concater: public Node<GroupInst, vector<int> > {
	vector<int> res;
	protected:
		void onBegin() {
			res.clear();
		}
		void process(GroupInst gi) {
			if (res.size() != varsNum + 1) {
				res.clear();
				res.resize(varsNum + 1);
			}
			for (int i = 1; i <= varsNum; i++)
				if (gi.vars[i] > 0)
					res[i] = 1;
				else if (gi.vars[i] < 0)
					res[i] = 0;
			gi.freeMem();
		}
		void preEnd() {
			sendNext(res);
		}
};

int _tmain(int argc, _TCHAR* argv[])
{
	if (argc < 3)
		return 1;
	Pipeline<std::pair<istream *, vector<Group> *>, vector<int> > pl(NodeWrapper<std::pair<std::istream *, vector<Group> *>, GroupInst>(new ReaderSplitter()) + NodeWrapper<GroupInst, GroupInst>(new SolverDPLL()) + NodeWrapper<GroupInst, vector<int> >(new Concater()));

	//while(1){
	double startTime = BaseServices::_Timer().getTimeD();
	std::ifstream in(argv[1], std::ios::in);
	vector<Group> myGroups;

	vector<int> res = pl.start(std::make_pair(&in, &myGroups))[0];
	for (size_t i = 0; i < myGroups.size(); i++)
		myGroups[i].freeMem();

	double workTime = BaseServices::_Timer().getTimeD() - startTime;
	if (res.size() > 1) {
		std::cout << "Solution exists! See file " << argv[2] << " for details" << std::endl;
		std::ofstream out(argv[2], std::ios::out);
		for (size_t i = 1; i < res.size(); i++)
			out << i << " " << (res[i] ? "T" : "F") << std::endl;
	} else
		std::cout << "Solution does not exist!" << std::endl;
	std::cout << "Time left: " << workTime / 1000 << " sec" << std::endl;
	//}
	return 0;
}
